$\forall$$T$:Type, $l$:($T$ List). no\_repeats($T$; $l$) $\in$ prop\{i:l\}